<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>PatternSynonyms3</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}
\usepackage{agda}
\begin{document}

</a><a id="61" class="Markup">\begin{code}</a>
<a id="74" class="Keyword">data</a> <a id="Nat"></a><a id="79" href="PatternSynonyms3.html#79" class="Datatype">Nat</a> <a id="83" class="Symbol">:</a> <a id="85" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="89" class="Keyword">where</a>
  <a id="Nat.zero"></a><a id="97" href="PatternSynonyms3.html#97" class="InductiveConstructor">zero</a> <a id="102" class="Symbol">:</a> <a id="104" href="PatternSynonyms3.html#79" class="Datatype">Nat</a>
  <a id="Nat.suc"></a><a id="110" href="PatternSynonyms3.html#110" class="InductiveConstructor">suc</a> <a id="114" class="Symbol">:</a> <a id="116" href="PatternSynonyms3.html#79" class="Datatype">Nat</a> <a id="120" class="Symbol">→</a> <a id="122" href="PatternSynonyms3.html#79" class="Datatype">Nat</a>

<a id="127" class="Keyword">pattern</a> <a id="two"></a><a id="135" href="PatternSynonyms3.html#135" class="InductiveConstructor">two</a>   <a id="141" class="Symbol">=</a> <a id="143" href="PatternSynonyms3.html#110" class="InductiveConstructor">suc</a> <a id="147" class="Symbol">(</a><a id="148" href="PatternSynonyms3.html#110" class="InductiveConstructor">suc</a> <a id="152" href="PatternSynonyms3.html#97" class="InductiveConstructor">zero</a><a id="156" class="Symbol">)</a>
<a id="158" class="Keyword">pattern</a> <a id="three"></a><a id="166" href="PatternSynonyms3.html#166" class="InductiveConstructor">three</a> <a id="172" class="Symbol">=</a> <a id="174" href="PatternSynonyms3.html#110" class="InductiveConstructor">suc</a> <a id="178" href="PatternSynonyms3.html#135" class="InductiveConstructor">two</a>
<a id="182" class="Keyword">pattern</a> <a id="four"></a><a id="190" href="PatternSynonyms3.html#190" class="InductiveConstructor">four</a>  <a id="196" class="Symbol">=</a> <a id="198" href="PatternSynonyms3.html#110" class="InductiveConstructor">suc</a> <a id="202" href="PatternSynonyms3.html#166" class="InductiveConstructor">three</a>

<a id="209" class="Keyword">pattern</a> <a id="five"></a><a id="217" href="PatternSynonyms3.html#217" class="InductiveConstructor">five</a>  <a id="223" class="Symbol">=</a> <a id="225" href="PatternSynonyms3.html#110" class="InductiveConstructor">suc</a> <a id="229" href="PatternSynonyms3.html#190" class="InductiveConstructor">four</a>

<a id="235" class="Keyword">data</a> <a id="Bot"></a><a id="240" href="PatternSynonyms3.html#240" class="Datatype">Bot</a> <a id="244" class="Symbol">:</a> <a id="246" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="250" class="Keyword">where</a>
<a id="256" class="Markup">\end{code}</a><a id="266" class="Background">

\end{document}
</a></pre></body></html>